T:Type, x:T. (x  [])  False 

latex

Definitions	prop{i:l}, t  T, A, A  B, P  Q, P  Q, P  Q, A c B, x:A. B(x), False, (x  l), P  Q, x:A. B(x), Y, ||as||,
Lemmas	false wf, select wf, length wf2, nat wf